Given the complex nature of, and the time consumed in analyzing hardware and software systems, there is an increasing need to provide debugging aids and diagnostic information which can be used to locate errors and ensure the correctness or verification of such systems.
Model checking has emerged as an effective technique for the automated analysis of software and hardware systems. Model checkers can analyze a system description automatically and provide a counterexample as feedback to the system designers. However, when analyzing software system descriptions, solely implementing a model checker for a complex problem rarely succeeds. As an alternative, theorem proving also affords an interesting approach. Conventional theorem proving systems, however, are often too general or too expensive to use in a practical setting because they require considerable user sophistication, human effort and system resources. Further, conventional theorem provers alone provide little or no diagnostic information when a theorem is not true.
One attempt to provide formal verification of systems is described in U.S. Pat. No. 5,481,717 to Gaboury. The Gaboury patent discloses a method for verifying a computer program in relation to a system specification. The implementation and specifications are translated to two finite state machine representations that are compared to each other in order to determine whether there exists an equivalence between internal states and values of the two finite state machine descriptions and whether said finite state machine descriptions produce equivalent respective output values for all equivalent input values. In accomplishing this verification method, Gaboury uses a method that is an extension of an existing Binary Decision Diagram (BDD). However, this approach has limited use in analyzing systems that contain integer constraints.
Another prior technique that provides formal verification of systems is an invariant checking method that combines binary decision diagrams (BDDs) with constraint solvers. This technique has the attributes of both a model checker and a theorem prover. The technique is automatic and provides counterexamples like the model checker, and like a theorem prover, the invariant checking method uses decision procedures and can handle infinite state systems. However, this invariant checking method does not provide for the efficient construction of a BDD in which the BDD employs optimized algorithms for obtaining optimal variable ordering. The prior art invariant checking method is described in Ramesh Bharadwaj and Steve Sims, “Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking, “TACAS 2000, which is hereby incorporated by reference.
Further prior art techniques use BDDs as a structure to represent a formula in propositional logic, i.e., logic that only involves variables of the boolean type. Such BDDs are only able to determine whether or not a formula, with only variables of boolean type, is always true or always false, and such techniques are unable to determine the truth or falsity of more complex formulas which may include variables of more complex types, such as, enumerations and integers in addition to boolean type. However, these conventional techniques determine variable ordering serendipitously or by random assignment and do not use optimized algorithms to obtain optimal variable ordering.